PossibleWorld(D;w)
== FairFifo
== & (i, x:Id. vartype(i;x)  M(i).ds(x))
== & & (i:Id, a:Action(i). isnull(a)  valtype(i;a)  M(i).da(kind(a)))
== & & (l:IdLnk, tg:Id. (w.M(l,tg))  M(source(l)).da(rcv(l,tg)))
== & & (i, x:Id. M(i).init(x,s(i;0).x))
== & & (i:Id, t:.
== & & (isnull(a(i;t))
== & & ( (islocal(kind(a(i;t)))  M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))))
== & & ( & (x:Id. M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x))
== & & ( & (l:IdLnk. M(i).send(kind(a(i;t));l;x.s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
== & & ( & (x:Id. M(i).frame(kind(a(i;t)) affects x)  s(i;t).x = s(i;t+1).x)
== & & ( & (l:IdLnk, tg:Id.
== & & ( & (M(i).sframe(kind(a(i;t)) sends <l,tg>)  w-tagged(tg;onlnk(l;m(i;t))) = nil))
== & & (i, a:Id, t:.
== & & (t':.
== & & (tt'
== & & (& isnull(a(i;t')) & kind(a(i;t')) = locl(a)
== & & (&  a declared in M(i)
== & & (&  unsolvable M(i).pre(a,x.s(i;t').x))
== & & & (i:Id, t:.
== & & & (isnull(a(i;t))  (x:Id. M(i).aframe(kind(a(i;t)) affects x)  s(i;t).x = s(i;t+1).x))
== & & & (i, x:Id, k:Knd. M(i).rframe(k reads x)  w-machine-independent(w;i;k;x))
== & & & (i:Id, t:.
== & & & (isnull(a(i;t))
== & & & ( (l:IdLnk. M(i).bframe(kind(a(i;t)) sends on l)  onlnk(l;m(i;t)) = nil)) 

latex

---

clarification:

possible-world{i:l}
possible-world(D; w)
== fair-fifo{i:l}
== fair-fifo(w)
== & (i:Id, x:Id. w-vartype(w; i; x)  d-m(D; i).ds(x))
== & & (i:Id, a:w-action(w; i).
== & & (w-isnull(w; a)  w-valtype(w; i; a)  d-m(D; i).da(w-kind(w; a)))
== & & (l:IdLnk, tg:Id. (w.M(l,tg))  d-m(D; source(l)).da(rcv(l,tg)))
== & & (i:Id, x:Id. d-m(D; i).init(x,w-s(w; i; 0; x)))
== & & (i:Id, t:.
== & & (w-isnull(w; w-a(w; i; t))
== & & ( (islocal(w-kind(w; w-a(w; i; t)))
== & & ( ( d-m(D; i).pre(act(w-kind(w; w-a(w; i; t))),
== & & ( ( x.w-s(w; i; t; x),w-val(w; w-a(w; i; t))))
== & & ( & (x:Id.
== & & ( & (d-m(D; i).ef(w-kind(w; w-a(w; i; t)),
== & & ( & (x,x.w-s(w; i; t; x),w-val(w; w-a(w; i; t)),w-s(w; i; (t+1); x)))
== & & ( & (l:IdLnk.
== & & ( & (d-m(D; i).send(w-kind(w; w-a(w; i; t));
== & & ( & (l;x.w-s(w; i; t; x);w-val(w; w-a(w; i; t));withlnk(l;w-m(w; i; t));i))
== & & ( & (x:Id.
== & & ( & (d-m(D; i).frame(w-kind(w; w-a(w; i; t)) affects x)
== & & ( & ( w-s(w; i; t; x) = w-s(w; i; (t+1); x)  d-m(D; i).ds(x))
== & & ( & (l:IdLnk, tg:Id.
== & & ( & (d-m(D; i).sframe(w-kind(w; w-a(w; i; t)) sends <l,tg>)
== & & ( & ( w-tagged(tg;onlnk(l;w-m(w; i; t))) = nil  w-Msg(w) List))
== & & (i:Id, a:Id, t:.
== & & (t':.
== & & (tt'
== & & (& w-isnull(w; w-a(w; i; t')) & w-kind(w; w-a(w; i; t')) = locl(a)  Knd
== & & (&  a declared in d-m(D; i)
== & & (&  unsolvable d-m(D; i).pre(a,x.w-s(w; i; t'; x)))
== & & & (i:Id, t:.
== & & & (w-isnull(w; w-a(w; i; t))
== & & & ( (x:Id.
== & & & ( (d-m(D; i).aframe(w-kind(w; w-a(w; i; t)) affects x)
== & & & ( ( w-s(w; i; t; x) = w-s(w; i; (t+1); x)  w-vartype(w; i; x)))
== & & & (i:Id, x:Id, k:Knd. d-m(D; i).rframe(k reads x)  w-machine-independent(w;i;k;x))
== & & & (i:Id, t:.
== & & & (w-isnull(w; w-a(w; i; t))
== & & & ( (l:IdLnk.
== & & & ( (d-m(D; i).bframe(w-kind(w; w-a(w; i; t)) sends on l)
== & & & ( ( onlnk(l;w-m(w; i; t)) = nil  w-Msg(w) List)) 

latex

Definitions

FairFifo, Action(i), valtype(i;a), f(a), w.M, M.da(a), source(l), rcv(l,tg), M.init(x,v), islocal(k), M.pre(a,s,v), act(k), M.ef(k,x,s,v,w), M.send(k;l;s;v;ms;i), val(a), withlnk(l;mss), M.frame(k affects x), M.ds(x), M.sframe(k sends <l,tg>), w-tagged(tg;mss), x:A. B(x), AB, A & B, locl(a), P  Q, a declared in M, unsolvable M.pre(a,s), x.A(x), M.aframe(k affects x), vartype(i;x), s(i;t).x, n+m, #$n, P & Q, Knd, M.rframe(k reads x), w-machine-independent(w;i;k;x), Id, , b, isnull(a), x:A. B(x), IdLnk, P  Q, A, M.bframe(k sends on l), M(i), kind(a), a(i;t), s = t, type List, Msg, onlnk(l;mss), m(i;t), nil

FDL editor aliases

p-world